Nuprl Definition : d-single-effect
0,22
postcript
pdf
@
i
: with declarations ds:
ds
da:
da
effect of
k
(v) is
x
:=
f
s v(
j
)
== if eqof(IdDeq)(
j
,
i
)
with declarations ds:
ds
da:
da
effect of
k
(v) is
x
:=
f
s v else fi
latex
Definitions
x
.
A
(
x
)
,
if
b
t
else
f
fi
,
f
(
a
)
,
eqof(
d
)
,
IdDeq
,
with declarations ds:
ds
da:
da
effect of
k
(v) is
x
:=
f
s v
,
FDL editor aliases
d-single-effect
origin
with declarations ds:dsda:daeffect of k(v) is x := f s v else fi 
x.A(x)